RCS "$Id: TranslateLogic.sig,v 1.11 1998/08/13 11:38:55 pxs Exp $";
(* As the logic used by the model checker is different from the logic        *)
(* visible to the user, a means of translating from the latter to the former *)
(* must be supplied.  This signature describes such a translator.            *)

signature TRANSLATE_LOGIC =
sig
   structure L   : MU_CALCULUS
   structure HML : LOGIC
     sharing L.M.A = HML.M.A
   val translate : L.prop -> HML.prop
end

